1. $T$ : Type
\\[0ex]2. $R$ : $T$$\rightarrow$$T$$\rightarrow\mathbb{P}$
\\[0ex]3. $\forall$$a$, $b$:$T$. Dec($R$($a$,$b$))
\\[0ex]4. $\forall$$a$, $b$:$T$. ($R$($a$,$b$) \& ($\neg$$R$($b$,$a$))) $\vee$ ($R$($a$,$b$) \& $R$($b$,$a$)) $\vee$ ($R$($b$,$a$) \& ($\neg$$R$($a$,$b$)))
\\[0ex]5. $x$ : $T$
\\[0ex]6. $y$ : $T$
\\[0ex]$\vdash$  $R$($x$,$y$) $\vee$ $R$($y$,$x$)